Skip to content

feat: define theorem for extractability for Merkle trees #144

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Open
BoltonBailey wants to merge 11 commits into
base: main
Choose a base branch
from
Open

feat: define theorem for extractability for Merkle trees #144

BoltonBailey wants to merge 11 commits into from

Conversation

@BoltonBailey
Copy link
Collaborator

@BoltonBailey BoltonBailey commented Sep 2, 2025 •
edited
Loading

This PR:

  • Refactors InductiveMerkleTree.lean into a folder, with existing work going into Defs.lean and Completeness.lean
  • Adds another Extractability.lean file with definition of the proof of extractability.
  • Makes some progress on the proof for this theorem

@github-actions
Copy link

github-actions bot commented Nov 9, 2025 •
edited
Loading

🤖 Gemini PR Summary

This diff significantly refactors and expands the Merkle Tree commitment scheme implementation.

Here is a high-level summary of the key changes:

  • Major Refactoring: The single InductiveMerkleTree.lean file has been split into a new MerkleTree directory with three more focused files:

    • Defs.lean: Contains the core definitions.
    • Completeness.lean: Contains the proof that valid proofs will always verify.
    • Extractability.lean: A new file introducing a key security proof.

  • Introduction of Extractability: The most significant change is the addition of a formal proof for the extractability of the Merkle tree. This is a crucial security property guaranteeing that if an adversary can successfully open a commitment, an "extractor" can recover the committed data from the adversary's interactions (i.e., its query log). This involves:

    • An extractor algorithm to reconstruct the tree.
    • A formal extractability_game to model adversarial attacks.
    • The statement of the main extractability theorem.

  • API Change: The verifyProof function was changed to return a Bool indicating success or failure, rather than failing the entire computation on an invalid proof. The completeness proof has been updated accordingly.

  • Helper Functions: New helper functions like leafCount and depth were added to the underlying Skeleton (binary tree) data structure to support the new proofs.

Analysis of Changes

Metric Count
📝 Files Changed 5
✅ Lines Added 460
❌ Lines Removed 74

sorry Tracking

  • ❌ Added: 3 sorry(s)
    • lemma OracleComp.bind_withLogging (A B) (spec : OracleSpec Unit) in ArkLib/CommitmentScheme/MerkleTree/Extractability.lean
    • theorem extractability [DecidableEq α] [SelectableType α] [Fintype α] [(spec α).FiniteRange] in ArkLib/CommitmentScheme/MerkleTree/Extractability.lean
    • lemma OracleComp.pure_withLogging (A B) (spec : OracleSpec Unit) in ArkLib/CommitmentScheme/MerkleTree/Extractability.lean

Last updated: 2025-12-11 02:32 UTC. See the main CI run for build status.

@BoltonBailey BoltonBailey changed the title Prove knowledge soundness for merkle trees feat: define theorem for extractability for Merkle trees Dec 11, 2025
@BoltonBailey BoltonBailey added the proof wanted A sorry to fill in label Dec 11, 2025
@github-actions
Copy link

github-actions bot commented Jan 19, 2026

🤖 Gemini PR Summary

As a senior engineer, here is a high-level summary of the changes in this PR. This work primarily focuses on formalizing the security properties of Merkle Trees—specifically extractability—while improving the project's modularity.

Features

  • Extractability Definition & Proof: Introduced Extractability.lean, which defines the formal extraction algorithm and the associated security game/theorem for Merkle trees.
  • Completeness Proofs: Established Completeness.lean to formally prove that validly generated Merkle proofs consistently verify against the tree root in both functional and monadic contexts.
  • Tree Meta-Data Helpers: Added new helper definitions to IndexedBinaryTree/Basic.lean for calculating the leaf count and depth of the Skeleton binary tree type.

Refactoring

  • Modular Architecture: Reorganized the inductive Merkle tree implementation from a single file into a dedicated directory structure (ArkLib/CommitmentScheme/MerkleTree/). This separates core definitions from their respective proofs (Completeness and Extractability).
  • API Simplification: Updated verifyProof in Defs.lean to return a boolean value, improving its usability as a predicate, and moved existing completeness theorems out of the core definition file to isolate concerns.
  • Import Management: Updated ArkLib.lean to reflect the new modular structure, ensuring the commitment scheme imports are streamlined.

Fixes

  • None reported in this PR.

Documentation

  • Formal documentation changes were not explicitly noted, though the introduction of the extraction security game provides implicit formal documentation of the system's security properties.

Analysis of Changes

Metric Count
📝 Files Changed 5
✅ Lines Added 460
❌ Lines Removed 74

sorry Tracking

❌ **Added:** 3 `sorry`(s)
  • lemma OracleComp.pure_withLogging (A B) (spec : OracleSpec Unit) in ArkLib/CommitmentScheme/MerkleTree/Extractability.lean
  • theorem extractability [DecidableEq α] [SelectableType α] [Fintype α] [(spec α).FiniteRange] in ArkLib/CommitmentScheme/MerkleTree/Extractability.lean
  • lemma OracleComp.bind_withLogging (A B) (spec : OracleSpec Unit) in ArkLib/CommitmentScheme/MerkleTree/Extractability.lean
🎨 **Style Guide Adherence**

ArkLib/CommitmentScheme/MerkleTree/Defs.lean

  • The file is missing a ## References section: "Each file that cites papers should have a ## References section in its docstring header"
  • Line 40: - See SNARGs book 29.2 for the "path-pruning" optimization. — "Use citation keys in text: Reference papers with citation keys like [ACFY24] rather than full titles or URLs."
  • Line 41: - See [here](https://eprint.iacr.org/2021/281.pdf#page=7.03) — "Use citation keys in text: Reference papers with citation keys like [ACFY24] rather than full titles or URLs."
  • Line 42: - [ ] Collision Lemma (See SNARGs book 18.3) — "Use citation keys in text: Reference papers with citation keys like [ACFY24] rather than full titles or URLs."
  • Line 44: - [ ] Extractability (See SNARGs book 18.5) — "Use citation keys in text: Reference papers with citation keys like [ACFY24] rather than full titles or URLs."

ArkLib/CommitmentScheme/MerkleTree/Extractability.lean

  • The file is missing a ## References section: "Each file that cites papers should have a ## References section in its docstring header"
  • Line 24: def OracleComp.withLogging — "Please follow the mathlib Style Guide... This covers naming conventions" (Mathlib 4 requires snake_case for functions/definitions).
  • Line 30: lemma OracleComp.pure_withLogging — "Please follow the mathlib Style Guide... This covers naming conventions" (Mathlib 4 requires snake_case for theorems/lemmas).
  • Line 44: lemma OracleComp.bind_withLogging — "Please follow the mathlib Style Guide... This covers naming conventions" (Mathlib 4 requires snake_case for theorems/lemmas).
  • Line 158: def collisionIn — "Please follow the mathlib Style Guide... This covers naming conventions" (Mathlib 4 requires snake_case for functions/definitions).
  • Line 162: Adapting from the SNARGs book Lemma 18.5.1: — "Use citation keys in text: Reference papers with citation keys like [ACFY24] rather than full titles or URLs."
  • Line 277: In the SNARGS book, they define — "Use citation keys in text: Reference papers with citation keys like [ACFY24] rather than full titles or URLs."
  • Line 285: The SNARGs book makes the observation that — "Use citation keys in text: Reference papers with citation keys like [ACFY24] rather than full titles or URLs."
📄 **Per-File Summaries**
  • ArkLib.lean: Reorganized the Merkle Tree commitment scheme imports by replacing the inductive implementation with modular components for definitions, completeness, and extractability.
  • ArkLib/CommitmentScheme/MerkleTree/Completeness.lean: Proves the completeness of inductive Merkle trees by showing that validly generated proofs always verify correctly against the tree's root in both functional and monadic contexts.
  • ArkLib/CommitmentScheme/MerkleTree/Defs.lean: Renames the file to Defs.lean and refactors verifyProof to return a boolean value, while removing completeness theorems to isolate the core Merkle tree definitions from their proofs.
  • ArkLib/CommitmentScheme/MerkleTree/Extractability.lean: Introduces the formal definition and proof of extractability for Merkle trees, including the extraction algorithm and its associated security game.
  • ArkLib/ToMathlib/Data/IndexedBinaryTree/Basic.lean: Added definitions for calculating the leaf count and depth of the Skeleton binary tree type.

Last updated: 2026-01-19 05:41 UTC.

@BoltonBailey BoltonBailey marked this pull request as ready for review January 19, 2026 05:46
@BoltonBailey
Copy link
Collaborator Author

BoltonBailey commented Jan 19, 2026 •
edited
Loading

I have only been able to work on this PR sporadically - it's looking like this PR will require more background on a collision lemma to be made sorry free. On the other hand, it does some reorganization of this folder, and so maybe it makes sense to merge now, so that any refactors don't overwrite the file and so people who are interested in the sorries can try to solve them.

What do you all think?

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

proof wanted A sorry to fill in

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@BoltonBailey